fifo-antecedent(es;Sys;f)
== e, e':E(Sys). (loc(e) = loc(e'))  f(e) loc f(e')   e loc e'  

latex

---

clarification:

fifo-antecedent(es;Sys;f)
== e:es-E-interface(es;Sys), e':es-E-interface(es;Sys).
== (es-loc(es; e) = es-loc(es; e')  Id)  es-le(es;f(e);f(e'))  es-le(es;e;e') 

latex

Up	abstract chain replication
Wellformedness Lemmas	fifo-antecedent wf
Definitions	x:A. B(x), E(X), s = t, Id, loc(e), P  Q, f(a), e loc e'
FDL editor aliases	fifo-antecedent